Termination Proof Script

• Consider the SCC {10}. There are no usable rules. By taking the AF π with π(REV1) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 10 is strictly decreasing.


• Consider the SCC {9,11,12}. By taking the AF π with π(rev) = π(REV) = 1, π(rev1) = π(rev2) = π(REV2) = 2, π(s) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence nil ≻ 0 and nil ≻ s, the rules in {1,2,6,7,11} are weakly decreasing and the rules in {3-5,9,12} are strictly decreasing.